k:Knd, l:IdLnk, dt:fpf(Id; x.Type).
(fpf-dom(Kind-deq; k; lnk-decl(l; dt)))
 guard(((isrcv(k)) c (fpf-dom(id-deq; tag(k); dt)))) 

latex

Definitions	b, tag(k), isrcv(k), x:A  B(x), left + right, Knd, t  T, IdLnk, Id, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), lnk-decl(l; dt), x.A(x), top, x:AB(x), Kind-deq, fpf-dom(eq; x; f), guard(T), P  Q, True, A c B, sq_type(T), s = t, prop{i:l}, sqequal(s; t), False
Lemmas	lnk-decl-dom-not, lnk-decl-dom2, IdLnk sq, lnk-decl-dom, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, Id wf, IdLnk wf, Knd wf